00100	x*y = if n x then y else a x . [d x . y]
00200	
00300	reverse x = rev[x,NIL]
00400	rev[x,y] = if n x then y else rev[d x, a x . y]
00500	
00600	reverse x = if n x then NIL else reverse[d x]*(a x)
00700	
00800	u ∪ v = if n u then v else if a u ε v then d u ∪ v
00900	else au.[du∪v]
01000	
01100	x ε u = ¬ n u ∧ [x eq a u ∨ x ε d u]
01200	xεu = ¬nu∧[x=au ∨ xεdu]
01300	
01400	x adjoin u = if xεu then u else x.u
01500	
01600	u∩v = if nu then NIL else if auεv then au.[du∩v] else du∩v
01700	
01800	inst[e,m,p] = if p eq NO then NO else if at m then [if isvar m then
01900	{assoc[m,p]⎇[λw. if n w then [m.e].p else if d w = e
02000	then p else NO] 
02100	else if m eq e then p else NO]
02200	else if at e then NO]
02300	else inst[d e,d m,inst[a e,a m,p]]
02400	
02500	sublis[e,p] = if at e then {assoc[e,p]⎇[λw. if n w then e else d w]]
02600	else {sublis[a e,p],sublis[d e,p]⎇[λx y. if x eq a e ∧
02700	y eq d e then e else x.y]